Over recent years, systems and software become more complicated, and their sizes are increasing. A verification method based on model checking is applied as one method for solving the increase in the complication and size. The model checking is a technique for creating a model that represents a verification object as a state transition system, and verifying whether the verification object satisfies specifications by comprehensively searching the state transition in the model. The model checking is applicable in a design stage and able to be applied to guarantee whether the verification object satisfies specifications. Therefore, the model checking is known as a noticeable technique for enhancing reliability of systems and software. Further, recently, the model checking is being attempted to be applied to verification of networks.
NPL 1, for example, discloses a technique for verifying, by model checking, a network controlled by a network control technique known as OpenFlow.
While having features as described above, the model checking includes a problem that memories and time necessary for calculation increase exponentially for a scale of a verification object. Therefore, in model checking intended to verify a practical system and software, it is necessary to execute searches efficiently.
NPL 2, for example, discloses a technique referred to as DPOR (Dynamic Partial Order Reduction). The DPOR is a technique for pruning a redundant search from the viewpoint of verification, in model checking for a multithread environment model. The DPOR first executes one arbitrary path when searching a state transition system as an object of model checking. The path is referred to as an execution path. The DPOR confirms whether a combination of transitions of which execution orders affect an execution result, is included in a transition series configuring the execution path. Such a combination of transitions is referred to as transitions having a dependence relation. When there are transitions with a dependence relation, the DPOR generates a backtrack point to search a path in which execution orders of the combination are switched. The backtrack point is generated in a state immediately before a transition previously made among the combination on the execution path. A search from the backtrack point is started from a point of making a transition (a transition different from the transition previously made among the combination) different from an execution path from the state to the last time. After detecting all the transitions with a dependence relation from the execution path and finishing generating a backtrack point in a state immediately before a transition previously made among the detected transitions, the DPOR re-starts a search from a last backtrack point in the execution path. This procedure is repeated until all backtrack points are searched.
Thereby, the DPOR is able to search only paths whose execution results are different, among all the execution patterns to be checked. In other words, the DPOR is able to execute searches efficiently, by pruning searches paths whose verification results are not different, for example,
NPL 3 discloses DPOR-DS (Dynamic Partial Order Reduction in Distributed Systems). The DPOR-DS is a technique that extends DPOR for model checking of a distributed environment model. In the DPOR-DS, to absorb a difference between environments relating to a model to be checked, a method for generating a backtrack point is changed. The DPOR-DS defines a happens-before relation in a distributed environment model with respect to a relation between transitions on an execution path, in addition to a dependence relation. The DPOR-DS applies the defined relation to determine generation of a backtrack point.
The happens-before relation is a relation regarding an execution order between transitions that is always satisfied in a certain model. For example, assuming transitions that transmit/receive a certain packet “p”. In this case, a transition that transmits the packet “p” happens always before a transition that receives the packet “p”. In this manner, a relation regarding an order between transitions always satisfied on the basis of a causal relation in a model is referred to as a happens-before relation.
In the DPOR-DS, in addition to a dependence relation, the presence or absence of a happens-before relation with regard to transitions on an execution path is also analyzed. A backtrack point is not generated by the DPOR-DS, when a happens-before relation is satisfied, even when there is a dependence relation between two transitions.
Further, in the DPOR-DS, when re-starting a search from a backtrack point, a happens-before relation for a combination of two transitions having a dependence relation is also considered. In the combination of two transitions having a dependence relation, assuming a case that a transition made former is designated as t1 and a transition made later is designated as t2. In this case, the DPOR-DS first continuously executes, in a search to be re-started, the transition t2 and a transition having a happens-before relation with the transition t2 among transitions made between the transitions t1 and t2.
FIG. 15 illustrates a specific example of re-starting a search from a backtrack point in the DPOR-DS. In FIG. 15, a circle represents a state of a model and an arrow represents a transition. It is assumed that in a first search, transitions are made in order of “ta”, “tb”, “tc”, and “td”. In addition, it is also assumed that, by analysis of a dependence relation, “ta” and “td” have been determined to have a dependence relation. Further, it is assumed that by analysis of a happens-before relation, “tc” and “td” have been determined to have a happens-before relation. In other words, the transition “tc” is always made before “td”.
The DPOR-DS generates a backtrack point “b1” in a state “s0” that is a state immediately before making “ta”. The DPOR-DS first makes, when re-starting a search from the backtrack point “b1”, transitions of “tc” and “td”. In other words, “tc” is a transition having the happens-before relation with the transition (“td”), which is made later in the combination having the dependence relation between transitions (“tb” and “tc”), among the combination of two transitions (“ta” and “td”) having the dependence relation. Further, “td” is a transition made later in the combination of two transitions having the dependence relation. In a re-search, an order of transitions thereafter is not determined, and an arbitrary path is searched and executed. In other words, in this example, for example, from the backtrack point “b1”, transitions are made in order of “tc”, “td”, “ta”, and “tb”. Among these transitions, first “tc” and “td” are a portion for which an order of executions is defined by a search algorism of the DPOR-DS, as described above. The remaining “ta” and “tb” are a portion for which an order of executions is arbitrarily determined. The definition of the order for the first portion is contrivance to reduce redundant searches.
FIG. 16 illustrates a case without that contrivance, as a specific example. Assuming a case in which only one transition (only “tc”) being made first on re-starting a search in backtracking is specified, in the above-described example. In this case, it may be possible to make transitions in order of “tc”, “ta”, “tb”, and “td” from the backtrack point “b1”. Intention of the re-start of the search from the backtrack point “b1” was to execute the search by switching orders of “ta” and “td” having the dependence relation, however in this search (a second search), these orders are not changed. In this case, a dependence relation is analyzed again for a path of “tc”, “ta”, “tb”, and “td”. In a state “s5” which is a state immediately before making “ta”, a backtrack point “b2” is generated. Thereby, in a next search from the backtrack point “b2”, is may be possible to execute a search (a third search) of a path causing transitions in a desired order of “tc”, “td”, “ta”, and “tb”.
However, in this case, the second search (a search of a path of “tc”, “ta”, “tb”, and “td”) is redundant from the viewpoint of verification and is needless from the viewpoint of efficiency. To reduce this redundant search, the DPOR-DS provides contrivance to specify a first transition sequence on re-starting a search by backtracking and to reduce a search of a redundant path. The specified first transition sequence includes “tc” and “td” in the above-described example. The reduced redundant path includes “tc”, “ta”, “tb”, and “td” in the above-described example. The DPOR-DS is able to prune, using these procedures, searches in model checking of a distributed environment model.
In addition, above-described NPL 1 describes a case which includes a transition with use of data (packets) when a state search is executed using model checking for a network controlled by OpenFlow. In other words, in such a transition, this related technique in NPL 1 executes symbolic execution for a program of an OpenFlow controller and thereby determines a set of representative values of packets capable of causing all transitions. The related technique searches a state using the determined data set. Such a data set is a set of packets such that when the OpenFlow controller program is executed using respective packets that are elements of the data set supplied as inputs, transitions based on all the operation patterns of the program can be made, as a result.
As described above, mainly in a test or a technique referred to as model checking, a method for determining a set of data to be used on the basis of symbolic execution of a program (or another technique for dividing data range) is referred to as a concolic technique. Further, handling data by the concolic technique is expressed as “handling data in a concolic manner.” Hereinafter, processing for determining a set of data to be used by the concolic technique will be also referred to as “concolic processing.”